{-# LANGUAGE TypeFamilies, FlexibleContexts, GADTs, TypeOperators #-}

{- |

Module      :  Type.Yoko.FunA
Copyright   :  (c) The University of Kansas 2011
License     :  BSD3

Maintainer  :  nicolas.frisby@gmail.com
Stability   :  experimental
Portability :  see LANGUAGE pragmas (... GHC)

"Type.Yoko.Fun" functions that /implicitly/ return an applicative functor. The
implicitness means that the 'Rng' type instance is not expected to include the
applicative functor.

-}

module Type.Yoko.FunA
  (Idiom, DomainA(..), applyA, applyAU) where

import Type.Yoko.Type
import Type.Yoko.Fun
import Type.Yoko.SetModel





type family Idiom (fn :: * -> *) :: * -> *
data DomainA fn t where
  AppABy :: (t ::: DomainA fn, True ~ (t ::? DomainA fn)) =>
            (fn t -> Dom fn t -> Idiom fn (Rng fn t)) -> DomainA fn t

instance SetModel (DomainA fn) where evidence AppABy{} x = x

applyA :: (t ::: DomainA fn) => fn t -> Dom fn t -> Idiom fn (Rng fn t)
applyA = applyAU membership

applyAU :: DomainA fn t -> fn t -> Dom fn t -> Idiom fn (Rng fn t)
applyAU (AppABy f) = f
